This pass simplifies definite iteration and non-linear patterns
by utilizing premises. This is done to make functions be able to
match the pattern matching of proof assistants.

It achieves this through the following steps:

• For non-linear patterns:
  • For each clause, we traverse the arguments and keep track
    of all variables in expressions. If a variable appears more
    than once, we generate a fresh version of the variable and
    keep it for later.
  • Once we have traversed the entire argument list, we use
    the variables tracked to generate new quantifiers and equality
    premises.
• For definite iteration:
  • For each clause, we traverse the arguments, and collect
    all variables used for definite iteration (i.e. the e in ListN e _ )
    and the respective lists being iterated.
  • Using the collected variables, we iterate through the list to create
    the equality premises.

For example (for non-linear pattern), take the function:

def $find(nat, nat* ) : bool
def $find(n, eps ) = false
def $find(n, n n'* ) = true
def $find(n, n_1 n'* ) = $find( n, n'* )

Would be transformed as such:

def $find(nat : nat, nat* ) : bool
def $find{n : nat}(n, []) = false
def $find{n : nat, `n'*` : nat*, n#1 : nat}(n, [n#1] ++ n'*{n' <- `n'*`}) = true
  -- if (n = n#1)
def $find{n : nat, n_1 : nat, `n'*` : nat*}(n, [n_1] ++ n'*{n' <- `n'*`}) = $find(n, n'*{n' <- `n'*`})

For definite iteration:

def $len( int* ) : nat
def $len(i^n) = n 

to

def $len(int* ) : nat
def $len{n : nat, `i*` : int*}(i^n{i <- `i*`}) = n
  -- if (n = |`i*`|)

Modified test.spectec with some cases (like the ones above).

For the definite iteration pass, it would actually make more sense to use a let premise. However, since it is not properly defined, an equality premise will have to do for now.